(set-logic QF_ABV)
(set-option :bv-solver bitblast-internal)
(set-option :check-models true)
(set-option :arrays-eager-lemmas true)
(set-info :status sat)
(declare-const a (Array (_ BitVec 64) (_ BitVec 64))) 
(declare-const b (_ BitVec 64)) 
(assert (= (store (store a b b) (select a b) (select a #x1111111111111111)) 
(store (store a #x1111111111111111 #x0000000000000000) (bvudiv b b) 
(bvadd b #x1111111111111111)))) 
(check-sat)
